Termination of the given ITRSProblem could successfully be proven:



↳ ITRS
  ↳ ITRStoIDPProof

ITRS problem:
The following domains are used:

z

The TRS R consists of the following rules:

sqBase(b, e, r) → halfExp(*@z(b, b), e, r)
condMod(TRUE, b, e, r) → sqBase(b, e, *@z(r, b))
halfExp(b, e, r) → condLoop(>@z(e, 0@z), b, /@z(e, 2@z), r)
condLoop(FALSE, b, e, r) → r
pow(b, e) → condLoop(>@z(e, 0@z), b, e, 1@z)
condLoop(TRUE, b, e, r) → condMod(=@z(%@z(e, 2@z), 1@z), b, e, r)
condMod(FALSE, b, e, r) → sqBase(b, e, r)

The set Q consists of the following terms:

sqBase(x0, x1, x2)
condMod(TRUE, x0, x1, x2)
halfExp(x0, x1, x2)
condLoop(FALSE, x0, x1, x2)
pow(x0, x1)
condLoop(TRUE, x0, x1, x2)
condMod(FALSE, x0, x1, x2)


Added dependency pairs

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof

I DP problem:
The following domains are used:

z

The ITRS R consists of the following rules:

sqBase(b, e, r) → halfExp(*@z(b, b), e, r)
condMod(TRUE, b, e, r) → sqBase(b, e, *@z(r, b))
halfExp(b, e, r) → condLoop(>@z(e, 0@z), b, /@z(e, 2@z), r)
condLoop(FALSE, b, e, r) → r
pow(b, e) → condLoop(>@z(e, 0@z), b, e, 1@z)
condLoop(TRUE, b, e, r) → condMod(=@z(%@z(e, 2@z), 1@z), b, e, r)
condMod(FALSE, b, e, r) → sqBase(b, e, r)

The integer pair graph contains the following rules and edges:

(0): SQBASE(b[0], e[0], r[0]) → HALFEXP(*@z(b[0], b[0]), e[0], r[0])
(1): CONDMOD(TRUE, b[1], e[1], r[1]) → SQBASE(b[1], e[1], *@z(r[1], b[1]))
(2): CONDLOOP(TRUE, b[2], e[2], r[2]) → CONDMOD(=@z(%@z(e[2], 2@z), 1@z), b[2], e[2], r[2])
(3): HALFEXP(b[3], e[3], r[3]) → CONDLOOP(>@z(e[3], 0@z), b[3], /@z(e[3], 2@z), r[3])
(4): POW(b[4], e[4]) → CONDLOOP(>@z(e[4], 0@z), b[4], e[4], 1@z)
(5): CONDMOD(FALSE, b[5], e[5], r[5]) → SQBASE(b[5], e[5], r[5])

(0) -> (3), if ((e[0] →* e[3])∧(r[0] →* r[3])∧(*@z(b[0], b[0]) →* b[3]))


(1) -> (0), if ((e[1] →* e[0])∧(*@z(r[1], b[1]) →* r[0])∧(b[1] →* b[0]))


(2) -> (1), if ((r[2] →* r[1])∧(b[2] →* b[1])∧(e[2] →* e[1])∧(=@z(%@z(e[2], 2@z), 1@z) →* TRUE))


(2) -> (5), if ((r[2] →* r[5])∧(b[2] →* b[5])∧(e[2] →* e[5])∧(=@z(%@z(e[2], 2@z), 1@z) →* FALSE))


(3) -> (2), if ((r[3] →* r[2])∧(b[3] →* b[2])∧(/@z(e[3], 2@z) →* e[2])∧(>@z(e[3], 0@z) →* TRUE))


(4) -> (2), if ((b[4] →* b[2])∧(e[4] →* e[2])∧(>@z(e[4], 0@z) →* TRUE))


(5) -> (0), if ((e[5] →* e[0])∧(r[5] →* r[0])∧(b[5] →* b[0]))



The set Q consists of the following terms:

sqBase(x0, x1, x2)
condMod(TRUE, x0, x1, x2)
halfExp(x0, x1, x2)
condLoop(FALSE, x0, x1, x2)
pow(x0, x1)
condLoop(TRUE, x0, x1, x2)
condMod(FALSE, x0, x1, x2)


As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(0): SQBASE(b[0], e[0], r[0]) → HALFEXP(*@z(b[0], b[0]), e[0], r[0])
(1): CONDMOD(TRUE, b[1], e[1], r[1]) → SQBASE(b[1], e[1], *@z(r[1], b[1]))
(2): CONDLOOP(TRUE, b[2], e[2], r[2]) → CONDMOD(=@z(%@z(e[2], 2@z), 1@z), b[2], e[2], r[2])
(3): HALFEXP(b[3], e[3], r[3]) → CONDLOOP(>@z(e[3], 0@z), b[3], /@z(e[3], 2@z), r[3])
(4): POW(b[4], e[4]) → CONDLOOP(>@z(e[4], 0@z), b[4], e[4], 1@z)
(5): CONDMOD(FALSE, b[5], e[5], r[5]) → SQBASE(b[5], e[5], r[5])

(0) -> (3), if ((e[0] →* e[3])∧(r[0] →* r[3])∧(*@z(b[0], b[0]) →* b[3]))


(1) -> (0), if ((e[1] →* e[0])∧(*@z(r[1], b[1]) →* r[0])∧(b[1] →* b[0]))


(2) -> (1), if ((r[2] →* r[1])∧(b[2] →* b[1])∧(e[2] →* e[1])∧(=@z(%@z(e[2], 2@z), 1@z) →* TRUE))


(2) -> (5), if ((r[2] →* r[5])∧(b[2] →* b[5])∧(e[2] →* e[5])∧(=@z(%@z(e[2], 2@z), 1@z) →* FALSE))


(3) -> (2), if ((r[3] →* r[2])∧(b[3] →* b[2])∧(/@z(e[3], 2@z) →* e[2])∧(>@z(e[3], 0@z) →* TRUE))


(4) -> (2), if ((b[4] →* b[2])∧(e[4] →* e[2])∧(>@z(e[4], 0@z) →* TRUE))


(5) -> (0), if ((e[5] →* e[0])∧(r[5] →* r[0])∧(b[5] →* b[0]))



The set Q consists of the following terms:

sqBase(x0, x1, x2)
condMod(TRUE, x0, x1, x2)
halfExp(x0, x1, x2)
condLoop(FALSE, x0, x1, x2)
pow(x0, x1)
condLoop(TRUE, x0, x1, x2)
condMod(FALSE, x0, x1, x2)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ IDP
              ↳ IDPNonInfProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(1): CONDMOD(TRUE, b[1], e[1], r[1]) → SQBASE(b[1], e[1], *@z(r[1], b[1]))
(5): CONDMOD(FALSE, b[5], e[5], r[5]) → SQBASE(b[5], e[5], r[5])
(2): CONDLOOP(TRUE, b[2], e[2], r[2]) → CONDMOD(=@z(%@z(e[2], 2@z), 1@z), b[2], e[2], r[2])
(3): HALFEXP(b[3], e[3], r[3]) → CONDLOOP(>@z(e[3], 0@z), b[3], /@z(e[3], 2@z), r[3])
(0): SQBASE(b[0], e[0], r[0]) → HALFEXP(*@z(b[0], b[0]), e[0], r[0])

(1) -> (0), if ((e[1] →* e[0])∧(*@z(r[1], b[1]) →* r[0])∧(b[1] →* b[0]))


(2) -> (5), if ((r[2] →* r[5])∧(b[2] →* b[5])∧(e[2] →* e[5])∧(=@z(%@z(e[2], 2@z), 1@z) →* FALSE))


(5) -> (0), if ((e[5] →* e[0])∧(r[5] →* r[0])∧(b[5] →* b[0]))


(3) -> (2), if ((r[3] →* r[2])∧(b[3] →* b[2])∧(/@z(e[3], 2@z) →* e[2])∧(>@z(e[3], 0@z) →* TRUE))


(2) -> (1), if ((r[2] →* r[1])∧(b[2] →* b[1])∧(e[2] →* e[1])∧(=@z(%@z(e[2], 2@z), 1@z) →* TRUE))


(0) -> (3), if ((e[0] →* e[3])∧(r[0] →* r[3])∧(*@z(b[0], b[0]) →* b[3]))



The set Q consists of the following terms:

sqBase(x0, x1, x2)
condMod(TRUE, x0, x1, x2)
halfExp(x0, x1, x2)
condLoop(FALSE, x0, x1, x2)
pow(x0, x1)
condLoop(TRUE, x0, x1, x2)
condMod(FALSE, x0, x1, x2)


The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair CONDMOD(TRUE, b[1], e[1], r[1]) → SQBASE(b[1], e[1], *@z(r[1], b[1])) the following chains were created:




For Pair CONDMOD(FALSE, b[5], e[5], r[5]) → SQBASE(b[5], e[5], r[5]) the following chains were created:




For Pair CONDLOOP(TRUE, b[2], e[2], r[2]) → CONDMOD(=@z(%@z(e[2], 2@z), 1@z), b[2], e[2], r[2]) the following chains were created:




For Pair HALFEXP(b[3], e[3], r[3]) → CONDLOOP(>@z(e[3], 0@z), b[3], /@z(e[3], 2@z), r[3]) the following chains were created:




For Pair SQBASE(b[0], e[0], r[0]) → HALFEXP(*@z(b[0], b[0]), e[0], r[0]) the following chains were created:




To summarize, we get the following constraints P≥ for the following pairs.



The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(CONDLOOP(x1, x2, x3, x4)) = -1 + x3   
POL(SQBASE(x1, x2, x3)) = -1 + x2   
POL(0@z) = 0   
POL(*@z(x1, x2)) = x1·x2   
POL(TRUE) = 2   
POL(2@z) = 2   
POL(FALSE) = -1   
POL(>@z(x1, x2)) = -1   
POL(CONDMOD(x1, x2, x3, x4)) = -1 + x3   
POL(=@z(x1, x2)) = -1   
POL(HALFEXP(x1, x2, x3)) = -1 + x2   
POL(1@z) = 1   
POL(undefined) = -1   

Polynomial Interpretations with Context Sensitive Arithemetic Replacement
POL(TermCSAR-Mode @ Context)

POL(%@z(x1, 2@z)-1 @ {}) = min{x2, (-1)x2}   
POL(%@z(x1, 2@z)1 @ {}) = max{x2, (-1)x2}   
POL(/@z(x1, 2@z)1 @ {CONDLOOP_4/2}) = -1 + max{x1, (-1)x1}   

The following pairs are in P>:

HALFEXP(b[3], e[3], r[3]) → CONDLOOP(>@z(e[3], 0@z), b[3], /@z(e[3], 2@z), r[3])

The following pairs are in Pbound:

HALFEXP(b[3], e[3], r[3]) → CONDLOOP(>@z(e[3], 0@z), b[3], /@z(e[3], 2@z), r[3])

The following pairs are in P≥:

CONDMOD(TRUE, b[1], e[1], r[1]) → SQBASE(b[1], e[1], *@z(r[1], b[1]))
CONDMOD(FALSE, b[5], e[5], r[5]) → SQBASE(b[5], e[5], r[5])
CONDLOOP(TRUE, b[2], e[2], r[2]) → CONDMOD(=@z(%@z(e[2], 2@z), 1@z), b[2], e[2], r[2])
SQBASE(b[0], e[0], r[0]) → HALFEXP(*@z(b[0], b[0]), e[0], r[0])

At least the following rules have been oriented under context sensitive arithmetic replacement:

*@z1 ↔
%@z1 →
/@z1 →


↳ ITRS
  ↳ ITRStoIDPProof
    ↳ IDP
      ↳ UsableRulesProof
        ↳ IDP
          ↳ IDependencyGraphProof
            ↳ IDP
              ↳ IDPNonInfProof
                ↳ IDP
                  ↳ IDependencyGraphProof

I DP problem:
The following domains are used:

z

R is empty.
The integer pair graph contains the following rules and edges:

(1): CONDMOD(TRUE, b[1], e[1], r[1]) → SQBASE(b[1], e[1], *@z(r[1], b[1]))
(5): CONDMOD(FALSE, b[5], e[5], r[5]) → SQBASE(b[5], e[5], r[5])
(2): CONDLOOP(TRUE, b[2], e[2], r[2]) → CONDMOD(=@z(%@z(e[2], 2@z), 1@z), b[2], e[2], r[2])
(0): SQBASE(b[0], e[0], r[0]) → HALFEXP(*@z(b[0], b[0]), e[0], r[0])

(1) -> (0), if ((e[1] →* e[0])∧(*@z(r[1], b[1]) →* r[0])∧(b[1] →* b[0]))


(2) -> (5), if ((r[2] →* r[5])∧(b[2] →* b[5])∧(e[2] →* e[5])∧(=@z(%@z(e[2], 2@z), 1@z) →* FALSE))


(5) -> (0), if ((e[5] →* e[0])∧(r[5] →* r[0])∧(b[5] →* b[0]))


(2) -> (1), if ((r[2] →* r[1])∧(b[2] →* b[1])∧(e[2] →* e[1])∧(=@z(%@z(e[2], 2@z), 1@z) →* TRUE))



The set Q consists of the following terms:

sqBase(x0, x1, x2)
condMod(TRUE, x0, x1, x2)
halfExp(x0, x1, x2)
condLoop(FALSE, x0, x1, x2)
pow(x0, x1)
condLoop(TRUE, x0, x1, x2)
condMod(FALSE, x0, x1, x2)


The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 4 less nodes.